Require Import AutoSep.

Fixpoint sll (ls : list W) (p : W) : HProp :=
  match ls with
    | nil => [| p = 0 |]
    | x :: ls' => [| p <> 0 |] * Ex p', (p ==*> x, p') * sll ls' p'
  end%Sep.

Definition tailS := SPEC("l") reserving 1
  Ex ls, 
  PRE[V] sll ls (V "l") * [| V "l" <> 0 |]
  POST[R] Ex a, Ex ls', [| ls = a::ls' |] * (V "l" ==*> a, R) * sll ls' R.

Definition tail := bmodule "tail"{{
  bfunction "tail"("l", "tmp")[tailS]
    "tmp" <- "l" + 4;;
    "tmp" <-* "tmp";;
    Return "tmp"
  end
}}.

Theorem tailOk : moduleOk tail.
Proof.
  vcgen.
  sep_auto.
  sep_auto.
  sep_auto.
  Lemma cons_fwd : forall(p:W)(ls:list W), p <> 0 -> sll ls p ===> Ex x, Ex ls', [| ls = x::ls' |] * Ex p', (p==*>x,p') * sll ls' p'.
    destruct ls; sepLemma.
  Qed.
  Definition hints : TacPackage.
    prepare cons_fwd tt.
  Defined.
  sep hints.
  sep hints.
Qed.